VERS5 
NIL 
((LISTINDUCTION LISPAX#28) (LISTINDUCTIONDEF LISPAX#32) (SEXPINDUCTION LISPAX#33) (SEXPINDUCTIONDEF LISPAX#34) (HIGH_ORDER_DEFINITION LISPAX#38) (LISTDEF LISPAX#43) (APPENDEF LISPAX#45) (LISTAPPEND LISPAX#46) (ALLPDEF LISPAX#50) (SOMEPDEF LISPAX#51) (MAPCARDEF LISPAX#52) (ALISTDEF LISPAX#55) (MKALIST LISPAX#56) (ASSOCDEF LISPAX#58) (MEMBERDEF LISPAX#61) (CONS_CAR_CDR LISPAX#26 LISPAX#27) (SIMPINFO LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#66 LISPAX#67)) (NIL . (DECL CAR (UNARYNAME: CAR) (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CAR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 950) (UNARY& . CAR)) . LISPAX#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 1 .)(NIL . (DECL CDR (UNARYNAME: CDR) (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CDR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 950) (UNARY& . CDR)) . LISPAX#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 2 .)(NIL . (DECL ATOM (UNARYNAME: ATOM) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ATOM . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . ATOM)) . LISPAX#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 3 .)(NIL . (DECL NULL (UNARYNAME: NULL) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((NULL . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . NULL)) . LISPAX#4 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 4 .)(NIL . (DECL LISTP (UNARYNAME: LISTP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((LISTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . LISTP)) . LISPAX#5 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 5 .)(NIL . (DECL ALISTP (UNARYNAME: ALISTP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ALISTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . ALISTP)) . LISPAX#6 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 6 .)(NIL . (DECL SEXP (UNARYNAME: SEXP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((SEXP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . SEXP)) . LISPAX#7 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 7 .)(NIL . (DECL (U V W) (TYPE: (TY& . GROUND)) (SORT: (TM& . LISTP))) . ((W . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) (V . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) (U . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) LISTP) . NIL . NIL . NIL . LISPAX . NIL . 8 .)(NIL . (DECL (X Y Z) (TYPE: (TY& . GROUND)) (SORT: (TM& . SEXP))) . ((Z . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) (Y . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) (X . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) SEXP) . NIL . NIL . NIL . LISPAX . NIL . 9 .)(NIL . (DECL (XA YA ZA) (TYPE: (TY& . GROUND)) (SORT: (TM& . ATOM))) . ((ZA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) (YA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) (XA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) ATOM) . NIL . NIL . NIL . LISPAX . NIL . 10 .)(NIL . (DECL (PHI) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((PHI . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#11 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 11 .)(NIL . (DECL CONS (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (SYNTYPE: CONSTANT) (INFIXNAME: |.|) (PREFIXNAME: CONS) (BINDINGPOWER: 850)) . ((CONS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 850) (PREFIX& . CONS) (INFIX& . |.|)) . LISPAX#12 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 12 .)(|∀XA.SEXP XA| . (AXIOM (TM& . |∀XA.SEXP XA|)) . (ATOM SEXP ZA YA XA) . NIL . (LISPAX#13) . NIL . LISPAX . NIL . 13 .)(|∀U.SEXP U| . (AXIOM (TM& . |∀U.SEXP U|)) . (LISTP SEXP W V U) . NIL . (LISPAX#14) . NIL . LISPAX . NIL . 14 .)(|∀X U.LISTP X.U| . (AXIOM (TM& . |∀X U.LISTP X.U|)) . (LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#15) . NIL . LISPAX . NIL . 15 .)(|∀U.¬NULL U⊃LISTP CDR U| . (AXIOM (TM& . |∀U.¬NULL U⊃LISTP CDR U|)) . (CDR NULL LISTP W V U) . NIL . (LISPAX#16) . NIL . LISPAX . NIL . 16 .)(|∀U.¬NULL U⊃SEXP CAR U| . (AXIOM (TM& . |∀U.¬NULL U⊃SEXP CAR U|)) . (CAR NULL LISTP SEXP W V U) . NIL . (LISPAX#17) . NIL . LISPAX . NIL . 17 .)(|∀X.¬ATOM X⊃SEXP CAR X| . (AXIOM (TM& . |∀X.¬ATOM X⊃SEXP CAR X|)) . (CAR ATOM SEXP Z Y X) . NIL . (LISPAX#18) . NIL . LISPAX . NIL . 18 .)(|∀X.¬ATOM X⊃SEXP CDR X| . (AXIOM (TM& . |∀X.¬ATOM X⊃SEXP CDR X|)) . (CDR ATOM SEXP Z Y X) . NIL . (LISPAX#19) . NIL . LISPAX . NIL . 19 .)(|∀X Y.SEXP X.Y| . (AXIOM (TM& . |∀X Y.SEXP X.Y|)) . (SEXP Z Y X CONS) . NIL . (LISPAX#20) . NIL . LISPAX . NIL . 20 .)(|∀X Y.¬ATOM X.Y| . (AXIOM (TM& . |∀X Y.¬ATOM X.Y|)) . (ATOM SEXP Z Y X CONS) . NIL . (LISPAX#21) . NIL . LISPAX . NIL . 21 .)(|∀X U.¬NULL X.U| . (AXIOM (TM& . |∀X U.¬NULL X.U|)) . (NULL LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#22) . NIL . LISPAX . NIL . 22 .)(|∀U.NULL U⊃U=NIL| . (AXIOM (TM& . |∀U.NULL U⊃U=NIL|)) . (NULL LISTP W V U) . NIL . (LISPAX#23) . NIL . LISPAX . NIL . 23 .)(|∀X Y.CAR (X.Y)=X| . (AXIOM (TM& . |∀X Y.CAR (X.Y)=X|)) . (CAR SEXP Z Y X CONS) . NIL . (LISPAX#24) . NIL . LISPAX . NIL . 24 .)(|∀X Y.CDR (X.Y)=Y| . (AXIOM (TM& . |∀X Y.CDR (X.Y)=Y|)) . (CDR SEXP Z Y X CONS) . NIL . (LISPAX#25) . NIL . LISPAX . NIL . 25 .)(|∀U.¬NULL U⊃CAR U.CDR U=U| . (AXIOM (TM& . |∀U.¬NULL U⊃CAR U.CDR U=U|)) . (CAR CDR NULL LISTP W V U CONS) . NIL . (LISPAX#26) . NIL . LISPAX . NIL . 26 .)(|∀X.¬ATOM X⊃CAR X.CDR X=X| . (AXIOM (TM& . |∀X.¬ATOM X⊃CAR X.CDR X=X|)) . (CAR CDR ATOM SEXP Z Y X CONS) . NIL . (LISPAX#27) . NIL . LISPAX . NIL . 27 .)(|∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))| . (AXIOM (TM& . |∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))|)) . (LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#28) . NIL . LISPAX . NIL . 28 .)(NIL . (DECL PARS (TYPE: (TY& . GROUND*))) . ((PARS . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#29 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 29 .)(NIL . (DECL (DF DF1 DF2) (TYPE: (TY& . |(GROUND⊗(GROUND*))→(GROUND*)|))) . ((DF2 . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#30 . NIL . VARIABLE .)) (DF1 . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#30 . NIL . VARIABLE .)) (DF . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#30 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 30 .)(NIL . (DECL NILCASE (TYPE: (TY& . |(GROUND*)→(GROUND*)|))) . ((NILCASE . (|(GROUND*)→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#31 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 31 .)(|∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧ FUN(X.U,PARS)= DEF(X,U,FUN(U,DF(X,PARS)),PARS)))| . (AXIOM (TM& . |∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧ FUN(X.U,PARS)= DEF(X,U,FUN(U,DF(X,PARS)),PARS)))|)) . (LISTP SEXP W V U Z Y X CONS PARS DF2 DF1 DF NILCASE (FUN . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .)) (DEF . (|(GROUND⊗GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .))) . NIL . (LISPAX#32) . NIL . LISPAX . NIL . 32 .)(|∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))| . (AXIOM (TM& . |∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))|)) . (ATOM SEXP Z Y X PHI CONS) . NIL . (LISPAX#33) . NIL . LISPAX . NIL . 33 .)(|∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y Z.(ATOM Z⊃ FUN(Z,PARS)=ATOMCASE(Z,PARS))∧ FUN(X.Y,PARS)= DEFSEXP(X,Y,FUN(X,DF1(X,Y,PARS)), FUN(Y,DF2(X,Y,PARS)), PARS)))| . (AXIOM (TM& . |∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y Z.(ATOM Z⊃ FUN(Z,PARS)=ATOMCASE(Z,PARS))∧ FUN(X.Y,PARS)= DEFSEXP(X,Y,FUN(X,DF1(X,Y,PARS)), FUN(Y,DF2(X,Y,PARS)), PARS)))|)) . (ATOM LISTP SEXP W V U Z Y X CONS PARS DF2 DF1 DF NILCASE FUN DEF (DEFSEXP . (|(GROUND⊗GROUND⊗GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#34 . NIL . VARIABLE .)) (ATOMCASE . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#34 . NIL . VARIABLE .))) . NIL . (LISPAX#34) . NIL . LISPAX . NIL . 34 .)(NIL . (DECL (ARB ARB1 ARB2) (TYPE: (TY& . ?ARBITRARY))) . ((ARB2 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#35 . NIL . VARIABLE .)) (ARB1 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#35 . NIL . VARIABLE .)) (ARB . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#35 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 35 .)(NIL . (DECL BIGFUN (TYPE: (TY& . |(GROUND⊗GROUND⊗(@ARB)⊗(@ARB))→(@ARB)|))) . ((BIGFUN . (|(GROUND⊗GROUND⊗(@ARB)⊗(@ARB))→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#36 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . LISPAX . NIL . 36 .)(NIL . (DECL (DEFINED_FUN ATOM_FUN) (TYPE: (TY& . |GROUND→(@ARB)|))) . ((ATOM_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .)) (DEFINED_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . LISPAX . NIL . 37 .)(|∀BIGFUN ATOM_FUN.(∃DEFINED_FUN.(∀X Y.(ATOM X⊃DEFINED_FUN(X)=ATOM_FUN(X))∧ DEFINED_FUN(X.Y)= BIGFUN(X,Y,DEFINED_FUN(X), DEFINED_FUN(Y))))| . (AXIOM (TM& . |∀BIGFUN ATOM_FUN.(∃DEFINED_FUN.(∀X Y.(ATOM X⊃DEFINED_FUN(X)=ATOM_FUN(X))∧ DEFINED_FUN(X.Y)= BIGFUN(X,Y,DEFINED_FUN(X), DEFINED_FUN(Y))))|)) . (ATOM SEXP Z Y X CONS ARB BIGFUN ATOM_FUN DEFINED_FUN) . NIL . (LISPAX#38) . NIL . LISPAX . NIL . 38 .)(NIL . (DECL LIST (TYPE: (TY& . |(GROUND*)→GROUND|)) (SYNTYPE: CONSTANT)) . ((LIST . (|(GROUND*)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#39 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 39 .)(NIL . (DECL LST (TYPE: (TY& . GROUND*))) . ((LST . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#40 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 40 .)(|LIST(())=NIL| . (AXIOM (TM& . |LIST(())=NIL|)) . (LIST) . NIL . (LISPAX#41) . NIL . LISPAX . NIL . 41 .)(|∀LST.LISTP LIST(LST)| . (AXIOM (TM& . |∀LST.LISTP LIST(LST)|)) . (LISTP LIST LST) . NIL . (LISPAX#42) . NIL . LISPAX . NIL . 42 .)(|∀X LST.LIST(X,LST)=X.LIST(LST)| . (AXIOM (TM& . |∀X LST.LIST(X,LST)=X.LIST(LST)|)) . (SEXP Z Y X CONS LIST LST) . NIL . (LISPAX#43) . NIL . LISPAX . NIL . 43 .)(NIL . (DECL APPEND (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (INFIXNAME: *) (BINDINGPOWER: 840)) . ((APPEND . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 840) (INFIX& . *)) . LISPAX#44 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 44 .)(|∀X U V.NIL*V=V∧X.U*V=X.(U*V)| . (DEFAX APPEND (TM& . |∀X U V.NIL*V=V∧X.U*V=X.(U*V)|)) . ((APPEND . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 840) (INFIX& . *)) . LISPAX#45 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#45) . NIL . LISPAX . NIL . 45 .)(|∀U V.LISTP U*V| . (AXIOM (TM& . |∀U V.LISTP U*V|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#46) . NIL . LISPAX . NIL . 46 .)(|∀U.U*NIL=U| . (AXIOM (TM& . |∀U.U*NIL=U|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#47) . NIL . LISPAX . NIL . 47 .)(|∀X V.X.NIL*V=X.V| . (AXIOM (TM& . |∀X V.X.NIL*V=X.V|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#48) . NIL . LISPAX . NIL . 48 .)(NIL . (DECL (ALLP SOMEP) (SYNTYPE: CONSTANT) (TYPE: (TY& . |((@PHI)⊗GROUND)→TRUTHVAL|))) . ((SOMEP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#49 . NIL . CONSTANT .)) (ALLP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#49 . NIL . CONSTANT .)) PHI) . NIL . NIL . NIL . LISPAX . NIL . 49 .)(|∀PHI X U.ALLP(PHI,NIL)∧ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)| . (DEFAX ALLP (TM& . |∀PHI X U.ALLP(PHI,NIL)∧ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)|)) . ((ALLP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#50 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X PHI CONS (SOMEP . LISPAX#49)) . NIL . (LISPAX#50) . NIL . LISPAX . NIL . 50 .)(|∀PHI X U.¬SOMEP(PHI,NIL)∧ SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))| . (DEFAX SOMEP (TM& . |∀PHI X U.¬SOMEP(PHI,NIL)∧ SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))|)) . ((SOMEP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#51 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#51) . NIL . LISPAX . NIL . 51 .)(|∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)| . (DEFAX MAPCAR (TM& . |∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)|)) . ((MAPCAR . (|((GROUND→GROUND)⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#52 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS (FN . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#52 . NIL . VARIABLE .))) . NIL . (LISPAX#52) . NIL . LISPAX . NIL . 52 .)(NIL . (DECL (ALIST) (TYPE: (TY& . GROUND)) (SORT: (TM& . ALISTP))) . ((ALIST . (GROUND . (SYMBOL& ALISTP NIL) . NIL . NIL . LISPAX#53 . NIL . VARIABLE .)) ALISTP) . NIL . NIL . NIL . LISPAX . NIL . 53 .)(|∀ALIST.LISTP ALIST| . (AXIOM (TM& . |∀ALIST.LISTP ALIST|)) . (LISTP ALISTP ALIST) . NIL . (LISPAX#54) . NIL . LISPAX . NIL . 54 .)(|∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)| . (AXIOM (TM& . |∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)|)) . (CAR ATOM NULL ALISTP ALIST) . NIL . (LISPAX#55) . NIL . LISPAX . NIL . 55 .)(|∀XA Y ALIST.ALISTP (XA.Y).ALIST| . (AXIOM (TM& . |∀XA Y ALIST.ALISTP (XA.Y).ALIST|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST) . NIL . (LISPAX#56) . NIL . LISPAX . NIL . 56 .)(NIL . (DECL ASSOC (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (SYNTYPE: CONSTANT)) . ((ASSOC . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#57 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 57 .)(|∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧ ASSOC(X,(XA.Y).ALIST)=(IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))| . (DEFAX ASSOC (TM& . |∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧ ASSOC(X,(XA.Y).ALIST)=(IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))|)) . ((ASSOC . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#58 . NIL . DEFINED .)) ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST) . NIL . (LISPAX#58) . NIL . LISPAX . NIL . 58 .)(|∀X ALIST.SEXP ASSOC(X,ALIST)| . (AXIOM (TM& . |∀X ALIST.SEXP ASSOC(X,ALIST)|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST ASSOC) . NIL . (LISPAX#59) . NIL . LISPAX . NIL . 59 .)(NIL . (DECL MEMBER (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((MEMBER . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#60 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 60 .)(|∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))| . (DEFAX MEMBER (TM& . |∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))|)) . ((MEMBER . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#61 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#61) . NIL . LISPAX . NIL . 61 .)(NIL . (DECL REVERSE (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (UNARYNAME: REVERSE)) . ((REVERSE . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((UNARY& . REVERSE)) . LISPAX#62 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 62 .)(|REVERSE NIL=NIL∧(∀X U.REVERSE (X.U)=REVERSE U*LIST(X))| . (DEFAX REVERSE (TM& . |REVERSE NIL=NIL∧(∀X U.REVERSE (X.U)=REVERSE U*LIST(X))|)) . (LISTP SEXP W V U Z Y X CONS LIST APPEND (REVERSE . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((UNARY& . REVERSE)) . LISPAX#63 . NIL . DEFINED .))) . NIL . (LISPAX#63) . NIL . LISPAX . NIL . 63 .)(NIL . (DECL REV1 (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (SYNTYPE: CONSTANT)) . ((REV1 . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#64 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 64 .)(|(∀V.REV1(NIL,V)=V)∧(∀X U V.REV1(X.U,V)=REV1(U,X.V))| . (DEFAX REV1 (TM& . |(∀V.REV1(NIL,V)=V)∧(∀X U V.REV1(X.U,V)=REV1(U,X.V))|)) . (LISTP SEXP W V U Z Y X CONS (REV1 . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#65 . NIL . DEFINED .))) . NIL . (LISPAX#65) . NIL . LISPAX . NIL . 65 .)(|∀U.LISTP REVERSE U| . (UE (UELST& (PHI . |λU.LISTP REVERSE U|)) (LN& . LISPAX#28) (OPEN REVERSE APPEND)) . (LISTP SEXP W V U Z Y X PHI CONS LIST APPEND REVERSE) . NIL . (LISPAX#63 LISPAX#28 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59) . NIL . LISPAX . NIL . 66 .)(|∀U V.LISTP REV1(U,V)| . (UE (UELST& (PHI . |λU.(∀V.LISTP REV1(U,V))|)) (LN& . LISPAX#28) (OPEN REV1)) . (LISTP SEXP W V U Z Y X PHI CONS REV1) . NIL . (LISPAX#63 LISPAX#65 LISPAX#28 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#41 LISPAX#42 LISPAX#43 LISPAX#45 LISPAX#46 LISPAX#47 LISPAX#48 LISPAX#54 LISPAX#59 LISPAX#66) . NIL . LISPAX . NIL . 67 .)